A, B:Type, xs:A List, ys:B List, x:A, y:B. (<x,y>  zip(xs;ys))  {(x  xs) & (y  ys)} 

latex

Definitions

t  T, type List, x:AB(x), x:AB(x), (x  l), P & Q, {T}, P  Q, x:A. B(x), Type, <a,b>, tl(l), n-m, if a<b c ; d fi, i<j, b, ij, Case b of inl(x)  s(x) ; inr(y)  t(y), if b t else f fi, nth_tl(n;as), hd(l), l[i], s = t, n+m, Case of a; nil  s ; x.y, rec:z  t(x;y;z), x.A(x), Y, ||as||, a<b, A, AB, , {x:A| B(x) }, , nil, False, P  Q, car.cdr, left+right, P  Q, zip(as;bs), Prop, P  Q, x. t(x), 1of(t), 2of(t)

Lemmas

pi2 wf, pi1 wf, and functionality wrt iff, cons member, zip wf, nil member, l member wf